0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 89 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 27 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇔, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
qB_in_g(0) → qB_out_g(0)
qB_in_g(s(0)) → qB_out_g(s(0))
qB_in_g(s(s(0))) → qB_out_g(s(s(0)))
qB_in_g(s(s(s(0)))) → qB_out_g(s(s(s(0))))
qB_in_g(s(s(s(s(0))))) → qB_out_g(s(s(s(s(0)))))
qB_in_g(s(s(s(s(s(0)))))) → qB_out_g(s(s(s(s(s(0))))))
qB_in_g(s(s(s(s(s(s(0))))))) → qB_out_g(s(s(s(s(s(s(0)))))))
qB_in_g(s(s(s(s(s(s(s(0)))))))) → qB_out_g(s(s(s(s(s(s(s(0))))))))
qB_in_g(s(s(s(s(s(s(s(s(T27))))))))) → U2_g(T27, pA_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
pA_in_gg(0, T35) → pA_out_gg(0, T35)
pA_in_gg(s(T40), T41) → U1_gg(T40, T41, pA_in_gg(T40, s(T41)))
U1_gg(T40, T41, pA_out_gg(T40, s(T41))) → pA_out_gg(s(T40), T41)
U2_g(T27, pA_out_gg(T27, s(s(s(s(s(s(s(0))))))))) → qB_out_g(s(s(s(s(s(s(s(s(T27)))))))))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
qB_in_g(0) → qB_out_g(0)
qB_in_g(s(0)) → qB_out_g(s(0))
qB_in_g(s(s(0))) → qB_out_g(s(s(0)))
qB_in_g(s(s(s(0)))) → qB_out_g(s(s(s(0))))
qB_in_g(s(s(s(s(0))))) → qB_out_g(s(s(s(s(0)))))
qB_in_g(s(s(s(s(s(0)))))) → qB_out_g(s(s(s(s(s(0))))))
qB_in_g(s(s(s(s(s(s(0))))))) → qB_out_g(s(s(s(s(s(s(0)))))))
qB_in_g(s(s(s(s(s(s(s(0)))))))) → qB_out_g(s(s(s(s(s(s(s(0))))))))
qB_in_g(s(s(s(s(s(s(s(s(T27))))))))) → U2_g(T27, pA_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
pA_in_gg(0, T35) → pA_out_gg(0, T35)
pA_in_gg(s(T40), T41) → U1_gg(T40, T41, pA_in_gg(T40, s(T41)))
U1_gg(T40, T41, pA_out_gg(T40, s(T41))) → pA_out_gg(s(T40), T41)
U2_g(T27, pA_out_gg(T27, s(s(s(s(s(s(s(0))))))))) → qB_out_g(s(s(s(s(s(s(s(s(T27)))))))))
QB_IN_G(s(s(s(s(s(s(s(s(T27))))))))) → U2_G(T27, pA_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
QB_IN_G(s(s(s(s(s(s(s(s(T27))))))))) → PA_IN_GG(T27, s(s(s(s(s(s(s(0))))))))
PA_IN_GG(s(T40), T41) → U1_GG(T40, T41, pA_in_gg(T40, s(T41)))
PA_IN_GG(s(T40), T41) → PA_IN_GG(T40, s(T41))
qB_in_g(0) → qB_out_g(0)
qB_in_g(s(0)) → qB_out_g(s(0))
qB_in_g(s(s(0))) → qB_out_g(s(s(0)))
qB_in_g(s(s(s(0)))) → qB_out_g(s(s(s(0))))
qB_in_g(s(s(s(s(0))))) → qB_out_g(s(s(s(s(0)))))
qB_in_g(s(s(s(s(s(0)))))) → qB_out_g(s(s(s(s(s(0))))))
qB_in_g(s(s(s(s(s(s(0))))))) → qB_out_g(s(s(s(s(s(s(0)))))))
qB_in_g(s(s(s(s(s(s(s(0)))))))) → qB_out_g(s(s(s(s(s(s(s(0))))))))
qB_in_g(s(s(s(s(s(s(s(s(T27))))))))) → U2_g(T27, pA_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
pA_in_gg(0, T35) → pA_out_gg(0, T35)
pA_in_gg(s(T40), T41) → U1_gg(T40, T41, pA_in_gg(T40, s(T41)))
U1_gg(T40, T41, pA_out_gg(T40, s(T41))) → pA_out_gg(s(T40), T41)
U2_g(T27, pA_out_gg(T27, s(s(s(s(s(s(s(0))))))))) → qB_out_g(s(s(s(s(s(s(s(s(T27)))))))))
QB_IN_G(s(s(s(s(s(s(s(s(T27))))))))) → U2_G(T27, pA_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
QB_IN_G(s(s(s(s(s(s(s(s(T27))))))))) → PA_IN_GG(T27, s(s(s(s(s(s(s(0))))))))
PA_IN_GG(s(T40), T41) → U1_GG(T40, T41, pA_in_gg(T40, s(T41)))
PA_IN_GG(s(T40), T41) → PA_IN_GG(T40, s(T41))
qB_in_g(0) → qB_out_g(0)
qB_in_g(s(0)) → qB_out_g(s(0))
qB_in_g(s(s(0))) → qB_out_g(s(s(0)))
qB_in_g(s(s(s(0)))) → qB_out_g(s(s(s(0))))
qB_in_g(s(s(s(s(0))))) → qB_out_g(s(s(s(s(0)))))
qB_in_g(s(s(s(s(s(0)))))) → qB_out_g(s(s(s(s(s(0))))))
qB_in_g(s(s(s(s(s(s(0))))))) → qB_out_g(s(s(s(s(s(s(0)))))))
qB_in_g(s(s(s(s(s(s(s(0)))))))) → qB_out_g(s(s(s(s(s(s(s(0))))))))
qB_in_g(s(s(s(s(s(s(s(s(T27))))))))) → U2_g(T27, pA_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
pA_in_gg(0, T35) → pA_out_gg(0, T35)
pA_in_gg(s(T40), T41) → U1_gg(T40, T41, pA_in_gg(T40, s(T41)))
U1_gg(T40, T41, pA_out_gg(T40, s(T41))) → pA_out_gg(s(T40), T41)
U2_g(T27, pA_out_gg(T27, s(s(s(s(s(s(s(0))))))))) → qB_out_g(s(s(s(s(s(s(s(s(T27)))))))))
PA_IN_GG(s(T40), T41) → PA_IN_GG(T40, s(T41))
qB_in_g(0) → qB_out_g(0)
qB_in_g(s(0)) → qB_out_g(s(0))
qB_in_g(s(s(0))) → qB_out_g(s(s(0)))
qB_in_g(s(s(s(0)))) → qB_out_g(s(s(s(0))))
qB_in_g(s(s(s(s(0))))) → qB_out_g(s(s(s(s(0)))))
qB_in_g(s(s(s(s(s(0)))))) → qB_out_g(s(s(s(s(s(0))))))
qB_in_g(s(s(s(s(s(s(0))))))) → qB_out_g(s(s(s(s(s(s(0)))))))
qB_in_g(s(s(s(s(s(s(s(0)))))))) → qB_out_g(s(s(s(s(s(s(s(0))))))))
qB_in_g(s(s(s(s(s(s(s(s(T27))))))))) → U2_g(T27, pA_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
pA_in_gg(0, T35) → pA_out_gg(0, T35)
pA_in_gg(s(T40), T41) → U1_gg(T40, T41, pA_in_gg(T40, s(T41)))
U1_gg(T40, T41, pA_out_gg(T40, s(T41))) → pA_out_gg(s(T40), T41)
U2_g(T27, pA_out_gg(T27, s(s(s(s(s(s(s(0))))))))) → qB_out_g(s(s(s(s(s(s(s(s(T27)))))))))
PA_IN_GG(s(T40), T41) → PA_IN_GG(T40, s(T41))
PA_IN_GG(s(T40), T41) → PA_IN_GG(T40, s(T41))
From the DPs we obtained the following set of size-change graphs: